a, b, c:. ((b = 0  ))  ((c = 0  ))  ((a/(b/c)) = (a * c/b)  ) 

latex

Definitions	P & Q, T, P  Q, P  Q, True, A, P  Q, (r/s), , t  T, P  Q, x:A. B(x), False, S  T
Lemmas	qmul assoc, qmul com, qmul-qdiv-cancel, qmul assoc qrng, qmul-qdiv-cancel4, qmul comm qrng, qmul one qrng, true wf, squash wf, qdiv wf, qinv-zero, qmul-zero, assert-qeq, qeq wf2, assert wf, qinv wf, qmul wf, not functionality wrt iff, int inc rationals, rationals wf, not wf